BadForcedIrrelevance.agda:10,16-17
Variable n is declared erased, so it cannot be used here
when checking that the expression n has type Nat
